\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$).
\-\\[0ex]normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ l\_all(\=ecl{-}kinds($A$);\+
\\[0ex]Knd;
\\[0ex]$k$.((($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$)) $\in$ Id)) $\wedge$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$)))
\\[0ex])
\-\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ msg{-}spec{-}loc{-}decl(${\it snd}$; $i$; ${\it da}$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=ecl{-}machine\=\{ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$);
\-\\[0ex]${\it es}$.ecl{-}mng\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$))
\-\-\-
\end{tabbing}